<html>
<head><meta charset="utf-8"><title>Specification language for Rust · wg-formal-methods · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/index.html">wg-formal-methods</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html">Specification language for Rust</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="243190702"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243190702" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243190702">(Jun 18 2021 at 17:46)</a>:</h4>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span></p>



<a name="243190818"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243190818" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243190818">(Jun 18 2021 at 17:46)</a>:</h4>
<p>I mean i agree, that having a shared language for even a subset of tools is desirable, but even in the simple 'law' example you presented there are highly non-trivial tradeoffs</p>



<a name="243190857"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243190857" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243190857">(Jun 18 2021 at 17:47)</a>:</h4>
<p>Have you looked at hte specifications of either my tool (Creusot) or Prusti?</p>



<a name="243190872"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243190872" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243190872">(Jun 18 2021 at 17:47)</a>:</h4>
<p>I've implemented my prototype language as a standalone crate</p>



<a name="243191176"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243191176" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243191176">(Jun 18 2021 at 17:50)</a>:</h4>
<p>And while I think that we should work to have a common language, perhaps one day converging towards an 'official' one, I worry about 'de facto' standardizing on the first / easiest thing. <br>
There are a few key questions on which i think different tools have different answers/perferences:</p>
<ul>
<li>Mutable borrows: How are the represented in specifications, what can you say?</li>
<li>Representations / Type invariants: Essential for modeling things like vec but very non-trivial </li>
<li>Marker traits, trait laws: There are also several tricky questions related to this, though I'll have a more complete story / answer to share in mid july after paper deadlines</li>
</ul>



<a name="243191475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243191475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243191475">(Jun 18 2021 at 17:54)</a>:</h4>
<p>I would love to discuss these issues with the rest of the Rust FV community, perhaps we're all in agreement on the best approaches to these problems, and if not I'm sure the disagreements will be stimulating/insightful.</p>



<a name="243192788"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243192788" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243192788">(Jun 18 2021 at 18:08)</a>:</h4>
<p><span class="user-mention" data-user-id="312719">@Xavier Denis</span> Reposting a bit of what I said in the other discussion so that others can see the law example</p>
<div class="codehilite"><pre><span></span><code>#[law]
fn R_is_reflexive(x: T) -&gt; bool { R(x, x) }
</code></pre></div>
<p>Clearly a limited format since it is limited to (implicit) universal quantification, is limited to what can be expressed in Rust, etc.<br>
But... also something that I could imagine a fuzzer checking, symbolic execution, BMC, abstract interpretation and interactive tools being used to prove. And clearly useful to interactive tools but also maybe useful to the automatic verifiers as well. (The last bit is a bit speculative)</p>
<p>Reminding myself what Prusti looks like from this paper (<a href="http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&amp;id=AstrauskasMuellerPoliSummers19b.pdf">http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&amp;id=AstrauskasMuellerPoliSummers19b.pdf</a>), it looks like #[requires/ensures/invariant/...] attributes containing a pure expression that can call pure functions, use quantifiers, use 'old' to refer to earlier values of an expression, etc.)<br>
(Is Creusot similar?)</p>
<p>I doubt very much that a (broadly construed) Rust FV community are in agreement about approach.<br>
But I think that there is value in trying to converge different corners to see what comes out of it.<br>
And I think that writing a spec for &lt;some tricky interesting thing that many people need a spec of&gt; (eg trait laws or bits of libstd) would<br>
1) Give us something that we could translate to some other notation or compare against another spec<br>
2) Highlight the limitations of whatever notation people happened to use.</p>



<a name="243193288"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243193288" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243193288">(Jun 18 2021 at 18:13)</a>:</h4>
<p>Creusot is _similar_ in the sense that it uses requires/ensures/invariant but the specification language is different.<br>
In particular we don't use pledges but instead have a special operator <code>^</code> (pronounced 'fin') which accesses the final value of a mutable borrow. Additionally, the grammar of Creusot is more flexible than that of prusti as it's based on a custom syn-parser,  but thats more of an implementation detail. </p>
<p>Given that Prusti and Creusot use widly different translations, I think we will diverge quite a bit on the questions of type invariants, whats possible, where and how. <br>
I also know that we have different solutions for traits based on the no longer implemented master's thesis on traits in Prusti and my own unimplemented approach (its on paper though!).</p>



<a name="243193457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243193457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243193457">(Jun 18 2021 at 18:15)</a>:</h4>
<p>I welcome discussion, I'm just wary of accidental lock-in, once a language is adopted by a tool, changing it is not a fun / easy task which can easily lead to defacto standardization.</p>



<a name="243193554"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243193554" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243193554">(Jun 18 2021 at 18:16)</a>:</h4>
<p>But a meeting where we present different ways of specifying some simple / interesting problems could be fun</p>



<a name="243201010"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243201010" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243201010">(Jun 18 2021 at 19:43)</a>:</h4>
<p>I get your point about accidental lock-in.<br>
I think the way to avoid that is for people to keep talking about what they are doing/planning, how it turned out, etc.</p>
<p>One of my memories of the Haskell committee (back when there were about 4 independent Haskell compilers/interpreters) was that we kept sharing examples and thinking about how we could take what other teams had done and implement something the same on our system. For some ideas, like GHC's rank-2 polymorphism, this was just fundamentally impossible for some typecheckers. For others like the foreign function call system it was challenging doing the same in a compiler and an interpreter but it was quickly obvious what we should do and what short-term hack we could use until we had the energy.  And for some things, we would suggest a change that made it easier to implement a feature on a broad range of implementations.</p>
<p>So I think we should try things out, try copying what others have done and/or talk about changes that make it easier to for multiple groups to implement. Some of the problems are obvious in advance (eg I have no clue what a symbolic execution tool or a fuzzer could possibly do with an existential quantifier) - but I bet that there is a lot of scope for shared syntax, shared specs, etc. as long as we share our ideas, design and experience and try to build on what the others are doing when we can.</p>



<a name="243301530"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243301530" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243301530">(Jun 20 2021 at 12:45)</a>:</h4>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span> hacspec now better integrates with proptest and quickcheck. However, the properties are not yet translated to the interactive backends. Could your proposal be helpful for hacspec?<br>
hacspec seems like the smallest non-trivial subset of rust, so it may be a good target to test ideas on.</p>



<a name="243308297"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243308297" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243308297">(Jun 20 2021 at 15:43)</a>:</h4>
<p><span class="user-mention" data-user-id="382207">@Bas Spitters</span> Yes, I think that the proptest API could be a good interface that many forms of verifier could use.</p>
<p>For those unfamiliar with proptest (<a href="https://altsysrq.github.io/proptest-book/proptest/tutorial/macro-proptest.html">https://altsysrq.github.io/proptest-book/proptest/tutorial/macro-proptest.html</a>), it basically adds two things:</p>
<ul>
<li>An Embedded Domain Specific Language (EDSL) for defining sets of values (including the usual collection operations: map, filter, etc.)</li>
<li>A macro proptest!{... fn f(a in S1, b in S2) } for writing universally quantified properties: drawing values a, b from the sets of values S1, S2.<br>
Properties fail by panicking on some input values: failing an assertion or overflow/bounds error/etc.</li>
</ul>
<p>We reimplemented the proptest API as part of our work with KLEE (See <a href="https://alastairreid.github.io/why-not-both/">https://alastairreid.github.io/why-not-both/</a> for a minimal example).<br>
Some things that we've used it to verify the obvious properties of base64 and some outputs of the Prost protobuf compiler - "forall x, decode(encode(x)) == x" and "forall x, decode(x) != panic". (And proptest has been used much more extensively.)</p>
<p>The way we implemented proptest should work for any verifier that has an API to create a symbolic value and to add assumptions about values.<br>
This should include other symbolic execution tools and bounded model checkers. (Our code is liberally licensed: <a href="https://github.com/project-oak/rust-verification-tools/tree/main/propverify">https://github.com/project-oak/rust-verification-tools/tree/main/propverify</a>)<br>
It obviously supports blackbox fuzz testing (that's what proptest uses).<br>
I think it could also support coverage-guided (greybox) fuzz testing (not tested - but don't see any obvious obstacle).</p>
<p>And, since it is just a universally quantified formula, I think that interactive tools would be able to support properties of this form - though it presumably needs some tooling to extract proptest!{...} to Coq/LEAN/etc .</p>



<a name="243309853"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243309853" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243309853">(Jun 20 2021 at 16:21)</a>:</h4>
<p>I'd need to look at the details, but I agree, it should hopefully be straightforward to translated those properties to the ITPs. One could even hope to prove some of them automatically (e.g. tactics in Coq, or SMT in EC, F*).</p>
<p>BTW have you looked at quickspec for haskell. It automatically proposes specifications using quick check. I guess the approach should work for some pure subset of rust too.</p>



<a name="243353670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243353670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243353670">(Jun 21 2021 at 08:40)</a>:</h4>
<p>Regarding the law example posted by <span class="user-mention" data-user-id="336739">@Alastair Reid</span>, it looks similar to listing 4 (page 3) of this Prusti project proposal: <a href="https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Johannes%20Schilling%20MS_Description.pdf">https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Johannes%20Schilling%20MS_Description.pdf</a></p>



<a name="243361353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243361353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alastair Reid <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243361353">(Jun 21 2021 at 10:05)</a>:</h4>
<p>Thanks for the link <span class="user-mention" data-user-id="116427">@Federico Poli</span> <br>
It's interesting that it seems that formulae are written in (a subset of) normal Rust syntax. eg listing 3 (page 2) writes quantifiers like this "forall(|i : usize| ...)". I don't see any examples like that in the OOPSLA 2019 paper - how did this evolve since then?</p>
<p>There is an interesting design choice for annotations/properties/formulae of whether</p>
<ol>
<li>They are written as an internal EDSL embedded in the Rust code (parsed and typechecker using the Rust typechecker) </li>
<li>They are written as an external EDSL with a custom parser, typechecker, etc. written in procedural macros, etc.<br>
Both choices have really strong pros/cons.</li>
</ol>
<p>(btw I should have said that I saw the #[law] syntax and the idea of using functions returning bool in an example by Georg Schmid at EPFL.)</p>



<a name="243364691"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243364691" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Bas Spitters <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243364691">(Jun 21 2021 at 10:45)</a>:</h4>
<p>hacspec uses the rust parser, but a standalone type checker. I could imagine such a hybrid approach could be useful for formulas too.</p>



<a name="243374653"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243374653" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243374653">(Jun 21 2021 at 12:29)</a>:</h4>
<p><span class="user-mention" data-user-id="336739">@Alastair Reid</span> The new syntax is described <a href="https://viperproject.github.io/prusti-dev/user-guide/verify/predicate.html">here</a>, it's indeed the rust-function-like <code>forall(|i : usize| ...)</code> quantification. The user guide at that link should be up-to-date with Prusti.</p>



<a name="243375003"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243375003" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Federico Poli <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243375003">(Jun 21 2021 at 12:32)</a>:</h4>
<p>Prusti annotations are implemented as procedural macros, which generate (dead) code that compiles only if the user-provided annotation type/borrow checks.</p>



<a name="243379910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/183875-wg-formal-methods/topic/Specification%20language%20for%20Rust/near/243379910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/183875-wg-formal-methods/topic/Specification.20language.20for.20Rust.html#243379910">(Jun 21 2021 at 13:16)</a>:</h4>
<p>In Creusot I chose to use a custom syntax for quantifiers: <code>forall&lt;binder:type&gt; prop</code>, it distinguishes it from normal functions rather than overloading similar but different concepts into the same syntax. <br>
Writing the proc macro isn't all that problematic and was needed anyways so that we can write prophetic assertions on mutable borrows</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>